(declare-const v0 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const _22-0 (_ BitVec 22))
(assert (and v0 (xor v0 v3 v0 v4 v3 v5)))
(push)
(assert (distinct (bvsgt _22-0 (bvnot _22-0)) (xor v0 v3 v0 v4 v3 v5)))
(pop)
(check-sat)
